Nuprl Definition : w-kindtype
11,40
postcript
pdf
w-kindtype(
TA
;
M
;
i
)(
k
)
== kindcase(
k
;
a
.
TA
(
a
);
l
,
tg
.if destination(
l
) =
i
then
M
(
l
,
tg
) else Void fi )
latex
Definitions
x
.
A
(
x
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
if
b
then
t
else
f
fi
,
a
=
b
,
destination(
l
)
,
f
(
a
)
,
Void
FDL editor aliases
w-kindtype
origin
x.A(x)x.A(x)